Nuprl Lemma : ma-body_wf
0,22
postcript
pdf
M
:MsgA. ma-body(
M
)
Shape(
M
)
latex
Definitions
t
T
,
da(
M
)
,
ds(
M
)
,
ma-body(
M
)
,
Shape(
M
)
,
x
:
A
B
(
x
)
,
MsgA
,
x
:
A
.
B
(
x
)
Lemmas
msga
wf
origin
M:MsgA. ma-body(M) 
Shape(M) M:MsgA. ma-body(M) Shape(M) T
B(x)x:A. B(x)